{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Type Checking\n",
    "### PPL 2020 http://www.cs.bgu.ac.il/~ppl202\n",
    "\n",
    "This lecture introduces *type checking* and *type inference* with illustration in TypeScript.\n",
    "\n",
    "* Introduce *optional type declarations* as illustrated in TypeScript\n",
    "* Define the *type language* defined in TypeScript - complex type definitions, named types, implicit types, recursive types, generic types\n",
    "* Define *function types*\n",
    "* Define closures and their types\n",
    "* Define *type compatibility* and *type checking*:\n",
    "* Distinguish *structural typing* and *nominal typing*"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Why Types\n",
    "\n",
    "Adding types to a program has three key advantages:\n",
    "* It allows the compiler to detect errors that would otherwise only be detected at runtime.\n",
    "  It is much better to detect errors as early as possible in the development cycle.\n",
    "* It serves as excellent documentation by reflecting the intention of the programmer.\n",
    "* More importantly, it helps the programmer **model** the solution she is designing.  A good typing system drives programs towards systematic models - both for data and for code.   \n",
    "\n",
    "Adding types is sometimes \"annoying\" because it can make programs longer, and for complicated types or generic types - it can\n",
    "make simple programs complex.  For example, a function such as `x => x` (known as the identity function) has a complex type\n",
    "(because it can work on any possible types).  We will see further examples of this later.\n",
    "\n",
    "TypeScript alleviates these 2 problems by:\n",
    "* Making type annotations optional.\n",
    "* Making type annotations implicit (that is, where the type of expressions can be inferred from the code, it will be).\n",
    "\n",
    "This approach is called **gradual typing**.  As a general strategy in programming languages, gradual typing allows programmers to trade-off prototyping and type safety."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Runtime Errors Caused by Unexpected Values"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Consider the following type definition and the function operating over values in this type:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[ 29, 25 ]"
      ]
     },
     "execution_count": 1,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "import {map} from 'ramda';\n",
    "\n",
    "interface Date {\n",
    "    year: number;\n",
    "    month: number;\n",
    "    day: number;\n",
    "};\n",
    "\n",
    "interface person {\n",
    "    birthDate: Date;\n",
    "    name: string;\n",
    "};\n",
    "\n",
    "const computeAges = persons => map(p=>2020-p.birthDate.year, persons);\n",
    "{\n",
    "    let persons = [{name:\"avi\", birthDate:{year:1991, month:7, day:10}}, \n",
    "                   {name:\"batia\", birthDate:{year:1995, month:3, day:2}}];\n",
    "    computeAges(persons)\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Consider now what happens if we invoke `computeAges` on this value:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "ename": "TypeError",
     "evalue": "Cannot read property 'year' of undefined",
     "output_type": "error",
     "traceback": [
      "evalmachine.<anonymous>:6",
      "var computeAges = function (persons) { return ramda_1.map(function (p) { return 2019 - p.birthDate.year; }, persons); };",
      "                                                                                                   ^",
      "",
      "TypeError: Cannot read property 'year' of undefined",
      "    at evalmachine.<anonymous>:6:100",
      "    at _map (C:\\ppl192\\node_modules\\ramda\\src\\internal\\_map.js:6:19)",
      "    at map (C:\\ppl192\\node_modules\\ramda\\src\\map.js:64:14)",
      "    at C:\\ppl192\\node_modules\\ramda\\src\\internal\\_dispatchable.js:41:15",
      "    at Object.f2 [as map] (C:\\ppl192\\node_modules\\ramda\\src\\internal\\_curry2.js:29:14)",
      "    at computeAges (evalmachine.<anonymous>:6:55)",
      "    at evalmachine.<anonymous>:1:1",
      "    at ContextifyScript.Script.runInThisContext (vm.js:50:33)",
      "    at Object.runInThisContext (vm.js:139:38)",
      "    at run ([eval]:1002:15)"
     ]
    }
   ],
   "source": [
    "computeAges([{name:\"avi\"}, {name:\"batia\"}])"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We obtain a runtime error when we try to access a property of a map which is not provided in the actual value passed \n",
    "to the function.  In other words, there is an incompatibility between the value passed to the function and the type\n",
    "of the value expected by the function.\n",
    "\n",
    "**Type annotations** are introduced in programming languages to enable **type checking**.\n",
    "Type checking is a process that analyzes a program and verifies that such incompatibities between \n",
    "variables or function parameters and the values to which they are bound at runtime are impossible\n",
    "for all possible executions of the program.\n",
    "\n",
    "When type checking is performed at compilation, it detects errors that could otherwise occur later at runtime.\n",
    "This is a much better situation - errors caught early are errors that are avoided.  Errors caught at \n",
    "runtime cause damage.\n",
    "\n",
    "Compilers that implement type checking provide an extremely powerful form of program verification."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Why would anyone give up on type checking?\n",
    "\n",
    "Given that type checking is such a powerful tool - why would any programmer want to give up this and use a programming language\n",
    "that does not provide it?\n",
    "\n",
    "The arguments usually advanced by proponents of languages without type checking are the following:\n",
    "* **Conciseness**: Programs without type annotations are more concise.  \n",
    "  Conciseness is important because it leads to more readability and better understanding.\n",
    "  \n",
    "  For example, the function above with types looks like:\n",
    "```\n",
    "const computeAges : (person:Person[])=>number[] = \n",
    "        persons => map(p=>2020-p.birthDate.year, persons);\n",
    "```\n",
    "  This argument is quite weak - because the additional type annotation is in fact a form of documentation\n",
    "  which clarifies the intention of the programmer.\n",
    "  \n",
    "  For example, consider the untyped function:\n",
    "```\n",
    "const add = (x,y)=>x+y;\n",
    "```\n",
    "  In Javascript, the `+` operator works on a wide range of values (number, strings, arrays).  It often produces unexpected output for example: \n",
    "```\n",
    "[1,2]+[\"a\", \"b\"] -> '1,2a,b'\n",
    "```\n",
    "  If a programmer declares that the intention of this function is to operate only over number, it clarifies the way the function can be tested and what it means for the function to be correct:\n",
    "```\n",
    "const add : (x:number, y:number)=>number = (x,y)=>x+y;\n",
    "```\n",
    "* **Untyped languages are easier to adjust to incremental changes.**\n",
    "\n",
    "For example, consider a program that operates over values of type `Person` as described above.\n",
    "If later, after the program has been put in production, we start introducing additional data for some persons - so that we add a new property `address`.  A program in an untyped language can be `patched` incrementally to support such values - by adding runtime checks for the presence of the additional property.  Such patching would require much more in-depth modifications in a statically type-checked language.\n",
    "\n",
    "* **Untyped languages encourage interactive programming.**\n",
    "\n",
    "When programmers interact with an interpreter, interactively, try a version of a function, then revise it, run tests,\n",
    "modify the structure of the values, revise the functions in fast experimentation cycles, with no compilation and direct\n",
    "interpretation - untyped languages allow faster experimentation.\n",
    "\n",
    "The counter argument is once the programmer has completed the experimentation / prototyping phase, the second stage of *cleaning up* with type definition can only improve the quality of the program and its design.  Gradual typing is attractive because it supports both types of operations and transition from prototype to typed correct versions.\n",
    "\n",
    "There are other arguments in favor of untyped languages which we will not develop further that are related \n",
    "to the type of polymorphism that is encouraged by each style.  In this course, we **strongly adopt the typed style of programming** (we have chosen our camp:)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Types in TypeScript\n",
    "\n",
    "TypeScript adds optional type declarations to JavaScript.\n",
    "\n",
    "The principles of this addition are:\n",
    "* Type declarations are optional.  If they are present, they are checked, otherwise no check is performed.\n",
    "  This means that regular JavaScript with no type annotations at all are valid TypeScript expressions.\n",
    "* The TypeScript compiler (`tsc`) performs two tasks:\n",
    "  * It translates a TypeScript program into a JavaScript program\n",
    "  * It checks that the program satisfies all the type declarations specified in the program.\n",
    "* Type annotations can be implicit and inferred by the TypeScript compiler. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "3"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "// The following TypeScript expression\n",
    "{\n",
    "    let add: (a:number, b:number)=>number = (a,b)=>a+b;\n",
    "    add(1,2);\n",
    "}\n",
    "\n",
    "// is translated by tsc into:\n",
    "{\n",
    "    let add = (a,b)=>a+b;\n",
    "    add(1,2);\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "*NOTE*: when there is a type error, the TypeScript compiler still outputs JavaScript code. We therefore do not see the \n",
    "type errors in these notebooks - as shown below:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'not ok'"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "// The type of variables can be *implicit*: \n",
    "// it is inferred automatically from the expression when possible\n",
    "{\n",
    "    let a = 43;\n",
    "    a = 'not ok'  \n",
    "    // Type error - a is a number variable\n",
    "    // it cannot be assigned a string value.\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To see these type errors, use one of the type editors which support TypeScript (we recommend VSCode as covered in Practical Sessions)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Type Annotations\n",
    "\n",
    "Type annotations are optional in TypeScript. They can occur in the following contexts:\n",
    "```\n",
    "// After variable declarations\n",
    "let var : <typeAnnotation>;  \n",
    "\n",
    "// As part of a function signature\n",
    "(param:<type>,...)=>...\n",
    "function fname(param : <typeAnnotation>, ...) : <typeAnnotation> { ... }\n",
    "```\n",
    "\n",
    "Type annotation are written in a specific form - which is called the **type language**.\n",
    "The type language is used to describe the expected type of variables, parameters or the value returned by functions.\n",
    "\n",
    "### Type Expression Denotation\n",
    "\n",
    "In general, all type expressions in the type language are used to refer to a specific set of values.\n",
    "The relation between a type expression and a set of values to which it corresponds is called **denotation**.\n",
    "(The denotation relation is in general the relation that exists between a *name* and the *object* to which the name refers.)\n",
    "\n",
    "\n",
    "### Atomic Type Expressions\n",
    "\n",
    "The simplest type language expression refers to a primitive type - for example `number`, `boolean`, `string`.\n",
    "\n",
    "It is used as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "true"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "{\n",
    "    let x:number = 2,\n",
    "        a:string = \"a\",\n",
    "        b:boolean = true;\n",
    "    b;\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "These atomic type expressions denote the primitive sets of values that are defined in Javascript (set of all number values, set of all string values, set of a boolean values).\n",
    "\n",
    "More complex type language expressions are needed to describe types over compound values.  These compound type expressions are constructed recursively by combining smaller type expressions"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Array Type Expressions\n",
    "\n",
    "To describe a homogeneous array, the following notation is used:\n",
    "`<typeAnnotation>[]`"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'a'"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "{\n",
    "    let stringArr : string[] = ['a', 'b', 'c'],\n",
    "        s : string = stringArr[0];\n",
    "    s;\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The following values are not compatible with this type annotation:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "true"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "stringArr = ['a', 1]  // Item 0 has wrong type\n",
    "stringArr[0] = true;  // Item 0 has wrong type"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Map Type Expressions\n",
    "\n",
    "To describe map types, the following notation is used:\n",
    "\n",
    "```{ <key>: <typeAnnotation>; ... }```"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{ name: 'avi', gender: 'm', cs: true, age: 22 }"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "{\n",
    "    let s : { name:string, cs:boolean, age:number } = { name:\"avi\", gender:\"m\", cs:true, age:22};\n",
    "    s;\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The expected meaning of the map type description is that **all the keys in the annotation must be present in the value with the described type.** \n",
    "\n",
    "There could be more keys as illustrated in the assignment `s=s2` below - but all the keys that are specified in the type must be present. \n",
    "\n",
    "Note, however, that when we bind a variable to a **literal expression**, the TypeScript compiler demands that the type of the literal be **exactly** that of the variable - with no extension.  "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{ name: 'avi', age: 22, cs: true, gender: 'm' }"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "{\n",
    "    let s : { name:string, cs:boolean, age:number } = { name:\"avi\", cs:true, age:22};\n",
    "    s = { age:22, name:\"avi\", cs:true};     // OK - The order of keys is not important\n",
    "    s = { name:\"avi\", age:22};              // Error: missing key \"cs\"\n",
    "    s = { name:\"avi\", age:\"22\", cs: true};  // Error: key \"age\" must be a string\n",
    "    s = { name:\"avi\", age:22, cs:true, gender:\"m\"}  // NOT OK for a literal because of additional key \"gender\"\n",
    "    {\n",
    "        let s2 : { name:string, cs:boolean, age:number, gender:string} = \n",
    "                 { name:\"avi\", age:22, cs:true, gender:\"m\"};\n",
    "        s = s2; // OK even though s2 has more properties - it satisfies the requirements of s's type.\n",
    "    }\n",
    "    s;\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Map Types Relationships\n",
    "\n",
    "The map type `{}` denotes all possible map values.\n",
    "\n",
    "The map type `{a:string}` denotes all maps that have a key `a` with a `string` value - for example:\n",
    "```\n",
    "{a:\"x\"}\n",
    "{a:\"y\", b:1}\n",
    "```\n",
    "and the following values are **not** part of this type:\n",
    "```\n",
    "{}\n",
    "{b:1}\n",
    "{a:1}\n",
    "```\n",
    "\n",
    "A map type `{a:string, b:number}` denotes all maps that have a key `a` with a `string` value and a key `b` with a `number` value.\n",
    "\n",
    "We infer from this definition that the type `{a:string, b:number}` is a strict **sub-type** of the type `{a:string}`.\n",
    "\n",
    "What is the relation between the types?\n",
    "```\n",
    "type mapAB = {a:string, b:number}\n",
    "type mapAC = {a:string, c:boolean}\n",
    "```\n",
    "\n",
    "These two types are distinct:\n",
    "```\n",
    "{a:\"x\", b:2} is in mapAB and not in mapAC\n",
    "{a:\"x\", c:true} is in mapAC and not in mapAB\n",
    "```\n",
    "Yet - they have a non-empty overlap:\n",
    "```\n",
    "{a:\"x\", b:2, c:true} is both in mapAB and in mapAC\n",
    "```\n",
    "\n",
    "In general - the intersection of the types `mapAB` and `mapAC` is the type:\n",
    "```\n",
    "type mapABC = {a:string, b:number, c:boolean}\n",
    "```\n",
    "\n",
    "The following types are disjoints:\n",
    "```\n",
    "type mapAS = {a:string}\n",
    "type mapAN = {a:number}\n",
    "```\n",
    "because the constraints on the value of the key `a` are incompatible.\n",
    "\n",
    "\n",
    "A good way to think about these relations is the following:\n",
    "* Each key:type component of the map type specification is a constraint on the values that belong to the type.\n",
    "* The more constraints are specified in a type, the less values belong to the type.\n",
    "* If you join all the constraints in two map type specifications - you obtain a type specification which denotes the *intersection* of the types (as long as the constraints are compatible)."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Named Type Expressions\n",
    "\n",
    "Type expressions can be given names.  For example, a map type expression can be named using the **interface** construct:\n",
    "\n",
    "```\n",
    "interface <typeName> {\n",
    "    <key>: <typeAnnotation>;\n",
    "    ...\n",
    "}\n",
    "```\n",
    "\n",
    "Other type constructs can be given a name using the **type** construct of the type language:\n",
    "```\n",
    "type <typeName> = <typeAnnotation>\n",
    "```"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{ name: 'avi', cs: true, age: 22 }"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "interface Student {\n",
    "    name: string;\n",
    "    cs: boolean;\n",
    "    age: number;\n",
    "}\n",
    "\n",
    "{\n",
    "    let s: Student = {name:\"avi\", cs:true, age:22};\n",
    "    type stringArray = string[];\n",
    "    s;\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Embedded Type Expressions\n",
    "\n",
    "A type expression can have arbitrary type expressions embedded recursively.\n",
    "For example:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{ name: 'avi',\n",
       "  cs: true,\n",
       "  age: 12,\n",
       "  courses: [ { courseName: 'ppl', dept: 'cs', semester: 2, year: 2017 } ] }"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "interface Course {\n",
    "    courseName: string;\n",
    "    dept: string;\n",
    "    semester: number;\n",
    "    year: number;\n",
    "};\n",
    "\n",
    "interface RegisteredStudent {\n",
    "    name: string;\n",
    "    cs: boolean;\n",
    "    age: number;\n",
    "    courses: Course[];\n",
    "};\n",
    "\n",
    "{\n",
    "    // This is a valid JSON value for the RegisteredStudent type\n",
    "    let rs : RegisteredStudent = {\n",
    "        name: \"avi\",\n",
    "        cs:true,\n",
    "        age:12,\n",
    "        courses: [{courseName: \"ppl\", dept:\"cs\", semester:2, year:2017}]\n",
    "    },\n",
    "\n",
    "    // This is NOT a valid JSON value for the RegisteredStudent type:\n",
    "    badRs : RegisteredStudent = {\n",
    "        name: \"avi\",\n",
    "        cs:true,\n",
    "        age:12,\n",
    "        courses: [{courseName: \"ppl\", dept:\"cs\", year:2017}] // badRs.courses[0] is missing key semester.\n",
    "    };\n",
    "    rs;\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The typescript compiler (tsc) emits this error:\n",
    "```\n",
    "(24,5): error TS2322: Type '{ name: string; cs: true; age: number; courses: { courseName: string; dept: string; year: number;...' is not assignable to type 'RegisteredStudent'.\n",
    "  Types of property 'courses' are incompatible.\n",
    "    Type '{ courseName: string; dept: string; year: number; }[]' is not assignable to type 'Course[]'.\n",
    "      Type '{ courseName: string; dept: string; year: number; }' is not assignable to type 'Course'.\n",
    "        Property 'semester' is missing in type '{ courseName: string; dept: string; year: number; }'.\n",
    "```\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Implicit Type Annotations\n",
    "\n",
    "Typescript can infer the type of variables based on their usage.  This is called an **implicit type annotation**.\n",
    "For example:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'nok'"
      ]
     },
     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "{\n",
    "    let a = 1;\n",
    "    a = 'nok'; // type error\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "On the assignment line `a = 'nok'`, tsc emits this error:\n",
    "\n",
    "```Type '\"s\"' is not assignable to type 'number'.\n",
    "```\n",
    "\n",
    "This means that tsc detected that the variable `a` is of type `number` based on its bound value `1`.\n",
    "From this point on, it checks that `a` keeps a `number` value."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Type Queries\n",
    "\n",
    "One can use the following notation to declare that a variable should have the type of another variable:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "ename": "Error",
     "evalue": "\tLine 3: Identifier expected.",
     "output_type": "error",
     "traceback": [
      "[COMPILE ERROR]",
      "\tLine 3: Identifier expected."
     ]
    }
   ],
   "source": [
    "{\n",
    "    let p1 = {name:\"avi\",age:22},\n",
    "        p2:typeof(p1) = {name:\"nok\"};\n",
    "    p2;\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In this case, tsc emits this error:\n",
    "```Type '{ name: string; }' is not assignable to type '{ name: string; age: number; }'.\n",
    "```\n",
    "\n",
    "Typescript detects that the type of `p1` is `{ name: string, age: number; }` on the basis of the value of `p1` - even though \n",
    "the type of `p1` was not declared - it was inferred from its value."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The `typeof(var)` construct is called a **type query** in TypeScript.\n",
    "\n",
    "**NOTE**: \n",
    "\n",
    "The `typeof(p1)` type query annotation is **different** from the `typeof` operator we discussed in the previous lecture - which is a primitive runtime operator in JavaScript.  \n",
    "\n",
    "The TypeScript `typeof` is a type annotation - it belongs to the Type Language - its value is a type annotation.\n",
    "\n",
    "The JavaScript `typeof` is a runtime primitive operator. Its value is a string."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "// JavaScript typeof\n",
    "const p3 = 2;\n",
    "typeof(p3);"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Recursive Types\n",
    "\n",
    "Consider the case of defining a binary tree.  Using JSON, we would encode a binary tree as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{ root: 1, left: { root: 2 }, right: { root: 3 } }"
      ]
     },
     "execution_count": 15,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "{\n",
    "    let binTree = {\n",
    "        root: 1,\n",
    "        left: { root: 2 },\n",
    "        right: { root: 3 }\n",
    "    };\n",
    "    binTree;\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The TypeScript type that corresponds to this value would be:\n",
    "```\n",
    "{   \n",
    "    root: number;\n",
    "    left: ?\n",
    "    right: ?\n",
    "}\n",
    "```\n",
    "We would need to specify that the `left` and `right` keys expect to receive values of exactly the same type.\n",
    "The only way to achieve such a declaration is to use a **recursive type declaration** -- which requires us to\n",
    "give a name to the type:\n",
    "\n",
    "```\n",
    "interface BinTree {\n",
    "    root: number;\n",
    "    left: BinTree;\n",
    "    right:BinTree;\n",
    "}\n",
    "```\n",
    "\n",
    "Let us try to create a value according to this type specification:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{ root: 1, left: { root: 2 }, right: { root: 3 } }"
      ]
     },
     "execution_count": 16,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "interface BinTree {\n",
    "    root: number;\n",
    "    left: BinTree;\n",
    "    right: BinTree;\n",
    "}\n",
    "\n",
    "let bn : BinTree = { // DOES NOT PASS TYPE CHECKING\n",
    "    root: 1,\n",
    "    left: { root: 2 },\n",
    "    right: { root: 3 }\n",
    "}\n",
    "bn"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Unfortunately, this value is not well typed - tsc returns this error:\n",
    "```\n",
    "Type '{ root: number; left: { root: number; }; right: { root: number; }; }' is not assignable to type 'BinTree'.\n",
    "  Types of property 'left' are incompatible.\n",
    "    Type '{ root: number; }' is not assignable to type 'BinTree'.\n",
    "      Property 'left' is missing in type '{ root: number; }'.\n",
    "```      \n",
    "\n",
    "That is - we are missing the keys `left` and `right` for the nodes with root 2 and 3.\n",
    "In other words, we cannot stop the recursion - the value must keep unrolling to be a valid BinTree.\n",
    "\n",
    "There are multiple solutions to this problem.  One is to indicate that the properties `left` and `right` are **optional**.\n",
    "This is indicated using the ? syntax as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{ root: 1,\n",
       "  left: { root: 2 },\n",
       "  right: { root: 3, right: { root: 4 } } }"
      ]
     },
     "execution_count": 17,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "interface BinTree {\n",
    "    root: number;\n",
    "    left?: BinTree;\n",
    "    right?: BinTree;\n",
    "}\n",
    "\n",
    "let bn : BinTree = {\n",
    "    root: 1,\n",
    "    left: { root: 2 },\n",
    "    right: { root: 3, \n",
    "             right: { root: 4}\n",
    "    }\n",
    "}\n",
    "bn"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Other solutions rely on **type unions** which we will review later in the course.\n",
    "\n",
    "**NOTE**:\n",
    "\n",
    "How different is the type annotation:\n",
    "`{a?: string, b:number}`\n",
    "from:\n",
    "`{a: any, b:number}`?\n",
    "\n",
    "**Answer**: the difference is that `a:any` means that the property `a` can have any possible value;\n",
    "in contrast `a?: string` means that either `a` does not occur at all or if it occurs it must have a value of type `string`."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Generic Types\n",
    "\n",
    "If we want to define a binary tree whose nodes can have any type - but where all the nodes in the tree must have the same type,\n",
    "we must introduce **type variables**.  "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{ root: 1, left: { root: 2 }, right: { root: 3 } }"
      ]
     },
     "execution_count": 18,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "interface BinTree<T> {\n",
    "    root: T,\n",
    "    left?: BinTree<T>,\n",
    "    right?: BinTree<T>\n",
    "}\n",
    "\n",
    "{\n",
    "    let bn : BinTree<number> = {\n",
    "        root: 1,\n",
    "        left: { root: 2 },\n",
    "        right: { root: 3 }\n",
    "    }\n",
    "    bn;\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "If we want to use a heterogeneous tree (a tree that can contain nodes of different types), we can use the special type\n",
    "called **`any`**:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "{ root: 'different', left: { root: 1, left: { root: false } } }"
      ]
     },
     "execution_count": 19,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "{\n",
    "    let an : BinTree<any> = {\n",
    "        root: 'different',\n",
    "        left: { root: 1,\n",
    "                left: { root : false }\n",
    "        }\n",
    "    };\n",
    "    an;\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The `any` type is compatible with all values - it denotes the set of all possible values.\n",
    "Every type that can be defined is actually a subset of the `any` type.\n",
    "In itself, `any` is not useful - typing a variable as `any` does not indicate any constraint on the variable.\n",
    "But when used as a type parameter in a complex type definition as above, `any` becomes useful."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### When are Generic Types useful?\n",
    "\n",
    "Generic types are compound type expressions with type variables.  Some of their components are thus left as unspecified types.\n",
    "When are such partially unspecified types useful?\n",
    "\n",
    "* One reason to define a generic type is to enable writing generic functions that operate over all possible instantiations of the generic type in the same manner.  For example, given a `BinTree` value, one can define generic functions such as `treeNodesNumber` or `treeDepth` which compute meaningful values over the value in exactly the same way regardless of the type of the node.  There would be no reason to write specific functions for a BinTreeOfString and a BinTreeOfNumber because the same algorithm works on these values."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "3"
      ]
     },
     "execution_count": 20,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "{\n",
    "    const treeNodesNumber : <T>(t:BinTree<T>)=>number = (t) => {\n",
    "        if (t === undefined)\n",
    "            return 0;\n",
    "        else return 1 + treeNodesNumber(t.left) + treeNodesNumber(t.right);\n",
    "    }\n",
    "    treeNodesNumber({ root: 1, left: { root: 2 }, right: { root: 3 } });\n",
    "}\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "3"
      ]
     },
     "execution_count": 21,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "{\n",
    "    const treeDepth : <T>(t:BinTree<T>)=>number = (t) => {\n",
    "        if (t === undefined)\n",
    "            return 0;\n",
    "        else return 1 + Math.max(treeDepth(t.left), treeDepth(t.right));\n",
    "    }    \n",
    "    treeDepth({ root: 1, left: { root: 2, left:{root:4}}, right: { root: 3 } })\n",
    "}\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "* Another reason to use generic types is when we need to define a set of value that is a combination between two types that are dependent of each other.  For example, consider the set of values which represent an array of values together with the minimum of the values that appear in the array.  Such data structure can be defined for any type `T` which denotes a set of values over which an order relation exists.  \n",
    "\n",
    "We can define it as generic type as follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'avi'"
      ]
     },
     "execution_count": 22,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "interface ArrayMin<T> {\n",
    "    min: T;\n",
    "    values: T[];\n",
    "}\n",
    "\n",
    "{\n",
    "    let numberArrayMin : ArrayMin<number> = {\n",
    "                min: 2,\n",
    "                values: [6,2,4]\n",
    "            },\n",
    "        stringArrayMin : ArrayMin<string> = {\n",
    "                min: \"avi\",\n",
    "                values: [\"bibi\", \"charles\", \"avi\"]\n",
    "            };\n",
    "        stringArrayMin.min;\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The relation between the two components of these values is the same - regardless of the actual type (number, string) of the components.\n",
    "\n",
    "Naturally, the two motivations for using generic types combine well together - generic algorithms work well over dependent components."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Generic Types Relationships\n",
    "\n",
    "What is the type relationship (inclusion, disjointness) between `BinTree<T>` and `BinTree<number>`?\n",
    "\n",
    "We first need to realize that the type expression `BinTree<T>` cannot be used as the type of a variable if it is not in the scope of a type variable.  That is, the expression:\n",
    "\n",
    "```\n",
    "{\n",
    "    let b : BinTree<T> = ...\n",
    "}\n",
    "```\n",
    "is not possible - because `BinTree<T>` cannot be in itself the type of a variable.  \n",
    "A generic type can only appear in the context of a generic function (like in the example `treeDepth` and `treeNodesNumber` above) or in the context of a larger generic type.\n",
    "\n",
    "When the tree variable is instantiated to a concrete (non-generic) type, then the type can be used as any other type:\n",
    "```\n",
    "{\n",
    "    let st : BinTree<string> = { root: \"avi\", left: { root: \"bibi\" } };\n",
    "    ...\n",
    "}\n",
    "```\n",
    "\n",
    "The relation between a generic type such as `BinTree<T>` and a type such as `BinTree<string>` is called **instantiation**.\n",
    "\n",
    "Now, what is the relation between `BinTree<string>` and `BinTree<number>`?\n",
    "These two concrete types are instances of the same generic type.\n",
    "Any value in `BinTree<string>` has a property `root` of type `string`.\n",
    "Any value in `BinTree<number>` has a property `root` of type `number`.\n",
    "We infer that these two types are **disjoint**.\n",
    "\n",
    "Note that while these two types are disjoint, we still can write generic functions that operate of values of either type using the same code.\n",
    "\n",
    "If a type `S` is a subtype of a type `T`, then what is the relation between the types `BinTree<S>` and `BinTree<T>`?\n",
    "For example, consider `T={name:string}` and `S={name:string,age:number}`.\n",
    "\n",
    "To answer this question, we can read the definition of `BinTree<T>` as a set of constraints a value must meet to belong to the type this type expression denotes:\n",
    "\n",
    "* The value must be a map value\n",
    "* A property `root` must be present and have a value of type T - which means that it must have a property `name` of type `string`.\n",
    "* A property `left` can either be absent or present and of type `BinTree<T>`\n",
    "* A property `right` can either be absent or present and of type `BinTree<T>`.\n",
    "\n",
    "Knowing that any value of type S is also a value of type T (by definition of subtyping), we can infer that any value in `BinTree<S>` meets all the constraints to also belong to `BinTree<T>`.\n",
    "\n",
    "In general, if `S` is a subtype of `T`, then `BinTree<S>` is a subtype of `BinTree<T>`."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Function Types\n",
    "\n",
    "One can type functions in TypeScript.  Let us introduce function types step by step:\n",
    "\n",
    "An untyped function in JavaScript has the following form:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 26,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "5\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "undefined"
      ]
     },
     "execution_count": 26,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "// Named function\n",
    "function add(x, y) {\n",
    "    return x + y;\n",
    "}\n",
    "\n",
    "{\n",
    "    // Anonymous function\n",
    "    const myAdd = function(x, y) { return x+y; };\n",
    "\n",
    "    // Using the fat arrow notation:\n",
    "    const myFatAdd = (x, y) => x+y;\n",
    "\n",
    "    console.log(myFatAdd(2,3));\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We can first specify the types of the parameters and the return type, in a way similar to the way it would be done in Java.\n",
    "This applies both to named functions and to anonymous functions."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "5\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "undefined"
      ]
     },
     "execution_count": 27,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "// Named function\n",
    "function add(x:number, y:number):number {\n",
    "    return x + y;\n",
    "}\n",
    "{\n",
    "    // Anonymous function\n",
    "    const myAdd = function(x:number, y:number):number { return x+y; };\n",
    "\n",
    "    // Using the fat arrow notation:\n",
    "    const myFatAdd = (x:number, y:number):number => x+y;\n",
    "    \n",
    "    console.log(myFatAdd(2,3));\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Let us now write the full type of the function out of the function value:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "7\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "undefined"
      ]
     },
     "execution_count": 28,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "{\n",
    "    let myAdd: (x: number, y: number)=>number =\n",
    "        function(x, y) { return x+y; };\n",
    "\n",
    "    let myFatAdd: (x: number, y: number)=>number =\n",
    "        (x,y)=>x+y;\n",
    "\n",
    "    console.log(myFatAdd(3,4));\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The type expression:\n",
    "```\n",
    "(x:number, y:number)=>number\n",
    "```\n",
    "is a **function type**.  The values that this type denotes are functions that map a pair of numbers to a number - in other words, functions whose domain is within $Number \\times Number$ and whose range is within $Number$. (Remember that types denote\n",
    "a set of values.)\n",
    "\n",
    "This notation is called the **function signature** - it combines the information on the type of the parameters, their name and \n",
    "the type of the returned value."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Parameter names are just to help with readability. \n",
    "We could have instead written:\n",
    "```\n",
    "let myAdd: (baseValue:number, increment:number) => number =\n",
    "    function(x: number, y: number): number { return x + y; };\n",
    "```\n",
    "As long as the parameter types align, itג€™s considered a valid type for the function, regardless of the names you give the parameters in the function type.\n",
    "\n",
    "The second part of the function type is the return type. We make it clear which is the return type by using a fat arrow (=>) between the parameters and the return type. This is a required part of the function type, so if the function doesnג€™t return a value (which means this is a function that just has a side-effect - no return value), we use the special type **`void`** \n",
    "instead of leaving it off."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Closures and their Type\n",
    "\n",
    "Consider the following function definition:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 29,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "13"
      ]
     },
     "execution_count": 29,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "{\n",
    "    let z = 10,\n",
    "        add : (x:number, y:number)=>number = (x,y)=>(x+y+z);\n",
    "    add(1,2);\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The definition of `add` refers to the variable `z`, which is defined outside the body of the function.\n",
    "When this happens, we say that the function **captures** the variable `z` - and the value of the function `add` is called\n",
    "a **closure**.  This is because the function *closes the captured variables* together with the function definition.\n",
    "\n",
    "The body of the function depends on the variable `z` - yet, the signature of the function does not indicate this dependency."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Consider the following example that indicates why this capture mechanism is part of the definition of the closure:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 30,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "15\n",
      "12\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "13"
      ]
     },
     "execution_count": 30,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "{\n",
    "    let adder = \n",
    "        function(inc) {\n",
    "            return x => x+inc;\n",
    "        },\n",
    "        a5 = adder(5),\n",
    "        a2 = adder(2);\n",
    "    \n",
    "    console.log(a5(10));\n",
    "    console.log(a2(10));\n",
    "    adder(10)(3);\n",
    "}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Let us analyze the defintion of the function `adder` - and refactor it step by step using types.\n",
    "\n",
    "`adder` is a function that accepts one parameter `inc`.\n",
    "What should be the type of `inc`?\n",
    "\n",
    "We look at where `inc` is used in the body of the function `adder` and find the expression `x+inc`. \n",
    "This expression appies to numbers - we conclude that `z` should be a `number`.\n",
    "\n",
    "The signature of the function `adder` should therefore look like:\n",
    "```\n",
    "(inc: number) => ?\n",
    "```\n",
    "\n",
    "What is the type of the value returned by `adder`?\n",
    "\n",
    "We analyze the body of `adder` to identify the returned expression:\n",
    "\n",
    "```\n",
    "    function(z) {\n",
    "        return x => x+inc;\n",
    "    }\n",
    "```\n",
    "\n",
    "The returned value is `x => x+inc`.\n",
    "This expression is a function - which receives `x` as a parameter and return `x+inc` as a parameter.\n",
    "\n",
    "The type of this returned function is thus:\n",
    "```\n",
    "(x:number) => number\n",
    "```\n",
    "\n",
    "Putting parameter and return value together, we obtain the type of the function `adder` as this expression:\n",
    "\n",
    "```\n",
    "(inc:number) => ((x:number) => number)\n",
    "```\n",
    "\n",
    "And adding all the types in the definition of `adder` we obtain:\n",
    "\n",
    "```\n",
    "let adder : (inc:number) => ((x:number)=>number) =\n",
    "    function(inc:number) {\n",
    "        return (x:number):number => x+inc;\n",
    "    }\n",
    "\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Now consider the **capturing of the parameter z** when the function `adder` is invoked - in the expression:\n",
    "\n",
    "```\n",
    "let add5 = adder(5);\n",
    "```\n",
    "\n",
    "The type of `add5` is `(x:number)=>number`.  `adder(5)` returns a function of one parameter.\n",
    "When it is invoked, this function adds 5 to its parameter.\n",
    "\n",
    "How does it know to add 5 specifically?\n",
    "\n",
    "This is because when the return function is computed, it **captures** the current value of the parameter `inc`.\n",
    "This happens in the computation of this expression:\n",
    "\n",
    "```\n",
    "Compute adder(5)\n",
    "Step 1: Bind parameter inc to 5\n",
    "Step 2: Compute the value (x => x+inc) **This is when variable inc is captured**\n",
    "```\n",
    "\n",
    "The key point is that when the value of the function is computed, `inc` is bound to the value 5.\n",
    "Later, when the value `add5` is used, `inc` is not bound anymore to any value - because the scope of its definition has been\n",
    "exited."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 31,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "7\n"
     ]
    },
    {
     "ename": "ReferenceError",
     "evalue": "inc is not defined",
     "output_type": "error",
     "traceback": [
      "evalmachine.<anonymous>:4",
      "    console.log(inc); // We confirm that inc is undefined",
      "                ^",
      "",
      "ReferenceError: inc is not defined",
      "    at evalmachine.<anonymous>:4:17",
      "    at ContextifyScript.Script.runInThisContext (vm.js:50:33)",
      "    at Object.runInThisContext (vm.js:139:38)",
      "    at run ([eval]:1002:15)",
      "    at onRunRequest ([eval]:829:18)",
      "    at onMessage ([eval]:789:13)",
      "    at emitTwo (events.js:126:13)",
      "    at process.emit (events.js:214:7)",
      "    at emit (internal/child_process.js:772:12)",
      "    at _combinedTickCallback (internal/process/next_tick.js:141:11)"
     ]
    }
   ],
   "source": [
    "{\n",
    "    let add5 = adder(5);\n",
    "        console.log(add5(2));  // add5 uses the value of inc which was captured when the closure was created\n",
    "        console.log(inc);      // We confirm that inc is undefined\n",
    "}   "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Type of Closures\n",
    "\n",
    "If we look back at the type of the closures returned when we compute `adder(5)` - we obtain:\n",
    "\n",
    "```\n",
    "(x:number)=>number\n",
    "```\n",
    "In words - it means that the value of `adder(5)` is a function which receives a number `x` and returns a number.\n",
    "\n",
    "Note that the closure does not indicate that it depends on another variable (`inc`) - because this is not part of the\n",
    "signature of the closure - it is an **internal** aspect of the closure."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Type Compatibility \n",
    "\n",
    "As part of the type checking performed by the TypeScript compiler, one must determine whether **two type expressions are\n",
    "compatible**.  This compatibility checking occurs in the following context for example:\n",
    "\n",
    "* Assume we know the type of a variable `a` to be a type expression `<type_a>`\n",
    "* We now compile the following expression: \n",
    "```\n",
    "let b : <type_b> = a; ...\n",
    "```\n",
    "At this point, the TypeScript compiler must determine whether `<type_a>` and `<type_b>` are compatible.\n",
    "\n",
    "* Similarly, assume we know the type of a function `f` to be `(x : <type_x>) => <type_y>`.\n",
    "* We now compile the following expression:\n",
    "```\n",
    "let z : <type_z> = v;\n",
    "    f(z)\n",
    "```\n",
    "At this point, the TypeScript compiler must determine whether `<type_x>` (the type of the formal parameter of function `f`) and `<type_z>` (the type of the actual variable passed as an argument to function `f`) are compatible."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Type Compatibility is NOT Symmetric: Subtyping\n",
    "\n",
    "Type compatibility is not symmetric - `T1` is compatible with `T2` means we can substitute a value of type `T2` with a value of type `T1` and still obtain valid expressions. The reverse may not be true.\n",
    "\n",
    "In general, think of type expressions as expressing **constraints** on the values that belong to the type.\n",
    "When a type expression `T1` expresses **more constraints** than `T2`, then it means the type expression `T1` denotes **less values** than `T2`.  It also means all the values in `T1` meet the constraints specified by `T2`.\n",
    "\n",
    "To remember this - we say that **`T1` is a subtype of `T2`** - all the values in `T1` satisfy the constraints of `T2`.\n",
    "When this is the case, it is safe to replace variables of type `T2` with values or variables of type `T1` - in short,\n",
    "it is safe to perform `let t2 = t1`.\n",
    "\n",
    "To remember the rule - remember: **`let t = s` is possible when `s < t`** - meaning \n",
    "we can bind with let (or pass as a parameter) a value or variable of type s to a variable of type t when s is a subtype of t.\n",
    "In this short form, s stands for source, t for target."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Compatibility Rules\n",
    "\n",
    "We will revisit the rules of type compatibility in Chapter 3.\n",
    "\n",
    "For now, consider the following practical aspects of type compatibility in TypeScript:\n",
    "\n",
    "* Primitive type expressions are compatible when they are the same (that is, `number` is compatible with `number` but not with `boolean` and not with `string`).  \n",
    "* Primitive type expressions are not compatible with any compound type expressions.  For example `number` is not compatible with `number[]` or with `{ x:number }`.\n",
    "* Arrays are only compatible with arrays, maps with maps, functions with functions.\n",
    "* Two array expressions `T1[]` and `T2[]` are compatible when `T1` and `T2` are compatible.\n",
    "\n",
    "The rules for maps and functions are a bit more complex: "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Map Type Compatibility: Structural Typing\n",
    "\n",
    "**Reference**: https://www.typescriptlang.org/docs/handbook/type-compatibility.html\n",
    "\n",
    "The basic rule of TypeScript for Map compatibility is:\n",
    "**`x` is compatible with `y` if `y` has at least the same members as `x`.**\n",
    "\n",
    "For example:\n",
    "```\n",
    "interface Named {\n",
    "    name: string;\n",
    "}\n",
    "\n",
    "let x: Named;\n",
    "// y's inferred type is { name: string; location: string; }\n",
    "let y = { name: \"Alice\", location: \"Seattle\" };\n",
    "x = y;\n",
    "```\n",
    "\n",
    "The type expression inferred for `y` is `{ name:string, location:string}`.\n",
    "It has more constraints than `Named`.\n",
    "\n",
    "In TypeScript, these two types are compatible - that is the type of `y` is a subtype of the `Named` type."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "To check whether `y` is compatible with the type of `x`, the compiler checks each property of `x` to find a corresponding compatible property in `y`. In this case, `y` must have a member called `name` that is a `string`. It does, so the assignment is allowed.\n",
    "\n",
    "The same rule for checking the compatibility of the assignment is used when checking function call arguments:\n",
    "```\n",
    "function greet(n: Named) {\n",
    "    console.log(\"Hello, \" + n.name);\n",
    "}\n",
    "greet(y); // OK\n",
    "```\n",
    "\n",
    "Note that `y` has an extra `location` property, but this does not create an error. \n",
    "Only members of the target type (`Named` in this case) are considered when checking for compatibility.\n",
    "\n",
    "This comparison process proceeds recursively, exploring the type of each member and sub-member."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This method of checking type compatibility is called **structural typing**. \n",
    "Structural typing is a way of relating types based solely on their members. \n",
    "This is in contrast with **nominal typing** which we know from Java and C++. \n",
    "\n",
    "Consider the following code:\n",
    "```\n",
    "interface Named {\n",
    "    name: string;\n",
    "}\n",
    "\n",
    "interface Person {\n",
    "    name: string;\n",
    "    age: number;\n",
    "}\n",
    "```\n",
    "\n",
    "Under structural typing, `Person` is a subtype of `Named` - even though this is not declared by the programmer; this subtyping relation is inferred by the compiler.\n",
    "\n",
    "```\n",
    "function greeter(n: Named):string {\n",
    "    return \"Hello \" + n.name;\n",
    "}\n",
    "\n",
    "let p : Person = { name:\"John\", age:26 }\n",
    "    greeter(p);  // OK because of structural typing: p declared as a subtype (Person) of Named\n",
    "```\n",
    "\n",
    "In **nominally-typed languages** like Java, the equivalent code would be an error because the Person type does not explicitly describe itself as being a subtype or an implementor of the Named interface - the programmer does not define explicitly relations between the types."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Function Types Compatibility: Comparing the Types of Functions\n",
    "\n",
    "(This is taken from https://www.typescriptlang.org/docs/handbook/type-compatibility.html):\n",
    "\n",
    "While comparing primitive types and object types is relatively straightforward, the question of what kinds of functions should be considered compatible is a bit more involved. Letג€™s start with a basic example of two functions that differ only in their parameter lists:\n",
    "\n",
    "```\n",
    "let x = (a: number, t: string) => 0;\n",
    "let y = (b: number, s: string) => 0;\n",
    "\n",
    "y = x; // OK\n",
    "```\n",
    "\n",
    "#### Comparing Parameters Types\n",
    "\n",
    "To check if x is assignable to y, we first look at the parameter list. Each parameter in `x` must have a corresponding parameter in `y` with a compatible type. Note that the names of the parameters are not considered, only their types. In this case, every parameter of `x` has a corresponding compatible parameter in `y`, so the assignment is allowed.\n",
    "\n",
    "We ignore here the complexity introduced by optional arguments and differing number of arguments - we will simplify by stating\n",
    "that two function parameter lists are compatible if they have the same length and the types of each parameters are compatible.\n",
    "\n",
    "#### Comparing Return Types\n",
    "\n",
    "Now letג€™s look at how return types are treated, using two functions that differ only by their return type:\n",
    "\n",
    "```\n",
    "let x = () => ({name: \"Alice\"});\n",
    "let y = () => ({name: \"Alice\", location: \"Seattle\"});\n",
    "\n",
    "x = y; // OK\n",
    "y = x; // Error because x() lacks a location property\n",
    "```\n",
    "\n",
    "The type system enforces that: **the source functionג€™s return type be a subtype of the target typeג€™s return type.**\n",
    "t = s\n",
    "s.r < t.r\n",
    "\n",
    "That is - when checking `f1 : (x:T1)=>U1` with `f2 : (x:T2)=>U2` - `f1` is a subtype of `f2` (meaning `f2 = f1` is ok) we verify that `U1` is a subtype of `U2`.\n",
    "\n",
    "The behavior of parameters and return values for function types when considering subtypes is well explained (with examples) in this post: \n",
    "https://www.stephanboyer.com/post/132/what-are-covariance-and-contravariance "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Summary\n",
    "\n",
    "### Types\n",
    "* **Types are useful** in programming languages:\n",
    "  * they allow the verification of type correctness at compile time instead of failing at runtime \n",
    "  * they are a reliable form of documentation of programs.\n",
    "* **Types in TypeScript are optional**.  The TypeScript compiler checks the types that are provided by the programmer and compiles the code to untyped JavaScript.\n",
    "* TypeScript type annotations are added in the following places in TypeScript expressions:\n",
    "```\n",
    "let var : <typeAnnotation>;  // After variable declarations\n",
    "function fname(param : <typeAnnotation>, ...) : <typeAnnotation> { ... } // As part of a function signature\n",
    "```\n",
    "\n",
    "### Type Language\n",
    "* TypeScript provides a **type language** to write type annotations.\n",
    "* **Primitive type expressions** are `number`, `boolean` and `string`\n",
    "* **Array type expressions** are of the form `T[]` where `T` can be any type expression.\n",
    "* **Map type expressions** are of the form `{ key: T, ...}` where `T` can be any type expression.\n",
    "* **Map type expressions can be given a name** in the form: `interface <name> <map-type-expression>`\n",
    "* **Type expressions can be embedded** into each other to specify the type of complex values like JSON types.\n",
    "* **Types can be implicit** and inferred by the TypeScript compiler in some cases.\n",
    "* **Recursive types** such as trees can be defined using **optional properties** in named map types.\n",
    "* **Generic types** can be defined using **type variables** in type expressions.  \n",
    "\n",
    "### Function Types\n",
    "* **Function types** specify the type of expected parameters and the return types. They are of the form `(x:T,...)=>T`.  This is called the **function signature**.\n",
    "* **Closures** may capture variable bindings - but these do not appear in their type - only the parameters and return values do.\n",
    "\n",
    "### Type Compatibility\n",
    "* A **source type expression $T_2$ is compatible with a target type expression $T_1$** when a variable declared with annotation $T_1$ can be bound to a value or variable of type $T_2$ (either through `let` or parameter passing to a function or assignment).\n",
    "This ensures that operations performed on the source value will be safe at runtime (for example, accessing a key in a map is an\n",
    "operation that is safe if the map types are compatible).\n",
    "* **Primitive types** are compatible when they are equal.\n",
    "* **Array types** are compatible when the element types are compatible.\n",
    "* **Map types** `x` and `y` are compatible when `y` has at least the same members as `x`.\n",
    "* **Map types** are checked **structurally** and **not nominally** in contrast to Java.\n",
    "* **Function types** are compatible when the parameter lists are compatible and the return types are compatible:\n",
    "  * The names of the parameters are ignored in the comparison.\n",
    "  * `(x:T1) => U1` is compatible with `(y:T2) => U2` if `T1 is compatible with T2` and `U2 is compatible with U1` (note the reversing). \n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "anaconda-cloud": {},
  "kernelspec": {
   "display_name": "Typescript 2.9",
   "language": "typescript",
   "name": "typescript"
  },
  "language_info": {
   "file_extension": ".ts",
   "mimetype": "text/x-typescript",
   "name": "typescript",
   "version": "2.9.2"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}